Step of Proof: sq_stable__and 9,38

Inference at * 
Iof proof for Lemma sq stable and:


  P,Q:. SqStable(P SqStable(Q SqStable(P  Q
latex

 by ((Unfold `sq_stable` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 
C3:n)) (first_tok :t) inil_term))) 
latex


C1

C1: 1. P : 
C1: 2. Q : 
C1: 3. (P P
C1: 4. (Q Q
C1: 5. (P  Q)
C1:   P
C2

C2: 1. P : 
C2: 2. Q : 
C2: 3. (P P
C2: 4. (Q Q
C2: 5. (P  Q)
C2:   Q
C.


Definitionst  T, P  Q, SqStable(P), P  Q, , x:AB(x)
Lemmassquash wf

origin